(0) Obligation:
Clauses:
rem(X, Y, R) :- ','(notZero(Y), ','(sub(X, Y, Z), rem(Z, Y, R))).
rem(X, Y, X) :- ','(notZero(Y), geq(X, Y)).
sub(s(X), s(Y), Z) :- sub(X, Y, Z).
sub(X, 0, X).
notZero(s(X)).
geq(s(X), s(Y)) :- geq(X, Y).
geq(X, 0).
Query: rem(g,g,a)
(1) PrologToDTProblemTransformerProof (SOUND transformation)
Built DT problem from termination graph DT10.
(2) Obligation:
Triples:
subD(s(X1), s(X2), X3) :- subD(X1, X2, X3).
geqC(s(X1), s(X2)) :- geqC(X1, X2).
remA(s(X1), s(X2), X3) :- subD(X1, X2, X4).
remA(X1, s(X2), X3) :- ','(subcB(X1, X2, X4), remA(X4, s(X2), X3)).
remA(s(X1), s(X2), s(X1)) :- geqC(X1, X2).
Clauses:
remcA(X1, s(X2), X3) :- ','(subcB(X1, X2, X4), remcA(X4, s(X2), X3)).
remcA(s(X1), s(X2), s(X1)) :- geqcC(X1, X2).
subcD(s(X1), s(X2), X3) :- subcD(X1, X2, X3).
subcD(X1, 0, X1).
geqcC(s(X1), s(X2)) :- geqcC(X1, X2).
geqcC(X1, 0).
subcB(s(X1), X2, X3) :- subcD(X1, X2, X3).
Afs:
remA(x1, x2, x3) = remA(x1, x2)
(3) TriplesToPiDPProof (SOUND transformation)
We use the technique of [DT09]. With regard to the inferred argument filtering the predicates were used in the following modes:
remA_in: (b,b,f)
subD_in: (b,b,f)
subcB_in: (b,b,f)
subcD_in: (b,b,f)
geqC_in: (b,b)
Transforming
TRIPLES into the following
Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:
REMA_IN_GGA(s(X1), s(X2), X3) → U3_GGA(X1, X2, X3, subD_in_gga(X1, X2, X4))
REMA_IN_GGA(s(X1), s(X2), X3) → SUBD_IN_GGA(X1, X2, X4)
SUBD_IN_GGA(s(X1), s(X2), X3) → U1_GGA(X1, X2, X3, subD_in_gga(X1, X2, X3))
SUBD_IN_GGA(s(X1), s(X2), X3) → SUBD_IN_GGA(X1, X2, X3)
REMA_IN_GGA(X1, s(X2), X3) → U4_GGA(X1, X2, X3, subcB_in_gga(X1, X2, X4))
U4_GGA(X1, X2, X3, subcB_out_gga(X1, X2, X4)) → U5_GGA(X1, X2, X3, remA_in_gga(X4, s(X2), X3))
U4_GGA(X1, X2, X3, subcB_out_gga(X1, X2, X4)) → REMA_IN_GGA(X4, s(X2), X3)
REMA_IN_GGA(s(X1), s(X2), s(X1)) → U6_GGA(X1, X2, geqC_in_gg(X1, X2))
REMA_IN_GGA(s(X1), s(X2), s(X1)) → GEQC_IN_GG(X1, X2)
GEQC_IN_GG(s(X1), s(X2)) → U2_GG(X1, X2, geqC_in_gg(X1, X2))
GEQC_IN_GG(s(X1), s(X2)) → GEQC_IN_GG(X1, X2)
The TRS R consists of the following rules:
subcB_in_gga(s(X1), X2, X3) → U13_gga(X1, X2, X3, subcD_in_gga(X1, X2, X3))
subcD_in_gga(s(X1), s(X2), X3) → U11_gga(X1, X2, X3, subcD_in_gga(X1, X2, X3))
subcD_in_gga(X1, 0, X1) → subcD_out_gga(X1, 0, X1)
U11_gga(X1, X2, X3, subcD_out_gga(X1, X2, X3)) → subcD_out_gga(s(X1), s(X2), X3)
U13_gga(X1, X2, X3, subcD_out_gga(X1, X2, X3)) → subcB_out_gga(s(X1), X2, X3)
The argument filtering Pi contains the following mapping:
remA_in_gga(
x1,
x2,
x3) =
remA_in_gga(
x1,
x2)
s(
x1) =
s(
x1)
subD_in_gga(
x1,
x2,
x3) =
subD_in_gga(
x1,
x2)
subcB_in_gga(
x1,
x2,
x3) =
subcB_in_gga(
x1,
x2)
U13_gga(
x1,
x2,
x3,
x4) =
U13_gga(
x1,
x2,
x4)
subcD_in_gga(
x1,
x2,
x3) =
subcD_in_gga(
x1,
x2)
U11_gga(
x1,
x2,
x3,
x4) =
U11_gga(
x1,
x2,
x4)
0 =
0
subcD_out_gga(
x1,
x2,
x3) =
subcD_out_gga(
x1,
x2,
x3)
subcB_out_gga(
x1,
x2,
x3) =
subcB_out_gga(
x1,
x2,
x3)
geqC_in_gg(
x1,
x2) =
geqC_in_gg(
x1,
x2)
REMA_IN_GGA(
x1,
x2,
x3) =
REMA_IN_GGA(
x1,
x2)
U3_GGA(
x1,
x2,
x3,
x4) =
U3_GGA(
x1,
x2,
x4)
SUBD_IN_GGA(
x1,
x2,
x3) =
SUBD_IN_GGA(
x1,
x2)
U1_GGA(
x1,
x2,
x3,
x4) =
U1_GGA(
x1,
x2,
x4)
U4_GGA(
x1,
x2,
x3,
x4) =
U4_GGA(
x1,
x2,
x4)
U5_GGA(
x1,
x2,
x3,
x4) =
U5_GGA(
x1,
x2,
x4)
U6_GGA(
x1,
x2,
x3) =
U6_GGA(
x1,
x2,
x3)
GEQC_IN_GG(
x1,
x2) =
GEQC_IN_GG(
x1,
x2)
U2_GG(
x1,
x2,
x3) =
U2_GG(
x1,
x2,
x3)
We have to consider all (P,R,Pi)-chains
Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES
(4) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
REMA_IN_GGA(s(X1), s(X2), X3) → U3_GGA(X1, X2, X3, subD_in_gga(X1, X2, X4))
REMA_IN_GGA(s(X1), s(X2), X3) → SUBD_IN_GGA(X1, X2, X4)
SUBD_IN_GGA(s(X1), s(X2), X3) → U1_GGA(X1, X2, X3, subD_in_gga(X1, X2, X3))
SUBD_IN_GGA(s(X1), s(X2), X3) → SUBD_IN_GGA(X1, X2, X3)
REMA_IN_GGA(X1, s(X2), X3) → U4_GGA(X1, X2, X3, subcB_in_gga(X1, X2, X4))
U4_GGA(X1, X2, X3, subcB_out_gga(X1, X2, X4)) → U5_GGA(X1, X2, X3, remA_in_gga(X4, s(X2), X3))
U4_GGA(X1, X2, X3, subcB_out_gga(X1, X2, X4)) → REMA_IN_GGA(X4, s(X2), X3)
REMA_IN_GGA(s(X1), s(X2), s(X1)) → U6_GGA(X1, X2, geqC_in_gg(X1, X2))
REMA_IN_GGA(s(X1), s(X2), s(X1)) → GEQC_IN_GG(X1, X2)
GEQC_IN_GG(s(X1), s(X2)) → U2_GG(X1, X2, geqC_in_gg(X1, X2))
GEQC_IN_GG(s(X1), s(X2)) → GEQC_IN_GG(X1, X2)
The TRS R consists of the following rules:
subcB_in_gga(s(X1), X2, X3) → U13_gga(X1, X2, X3, subcD_in_gga(X1, X2, X3))
subcD_in_gga(s(X1), s(X2), X3) → U11_gga(X1, X2, X3, subcD_in_gga(X1, X2, X3))
subcD_in_gga(X1, 0, X1) → subcD_out_gga(X1, 0, X1)
U11_gga(X1, X2, X3, subcD_out_gga(X1, X2, X3)) → subcD_out_gga(s(X1), s(X2), X3)
U13_gga(X1, X2, X3, subcD_out_gga(X1, X2, X3)) → subcB_out_gga(s(X1), X2, X3)
The argument filtering Pi contains the following mapping:
remA_in_gga(
x1,
x2,
x3) =
remA_in_gga(
x1,
x2)
s(
x1) =
s(
x1)
subD_in_gga(
x1,
x2,
x3) =
subD_in_gga(
x1,
x2)
subcB_in_gga(
x1,
x2,
x3) =
subcB_in_gga(
x1,
x2)
U13_gga(
x1,
x2,
x3,
x4) =
U13_gga(
x1,
x2,
x4)
subcD_in_gga(
x1,
x2,
x3) =
subcD_in_gga(
x1,
x2)
U11_gga(
x1,
x2,
x3,
x4) =
U11_gga(
x1,
x2,
x4)
0 =
0
subcD_out_gga(
x1,
x2,
x3) =
subcD_out_gga(
x1,
x2,
x3)
subcB_out_gga(
x1,
x2,
x3) =
subcB_out_gga(
x1,
x2,
x3)
geqC_in_gg(
x1,
x2) =
geqC_in_gg(
x1,
x2)
REMA_IN_GGA(
x1,
x2,
x3) =
REMA_IN_GGA(
x1,
x2)
U3_GGA(
x1,
x2,
x3,
x4) =
U3_GGA(
x1,
x2,
x4)
SUBD_IN_GGA(
x1,
x2,
x3) =
SUBD_IN_GGA(
x1,
x2)
U1_GGA(
x1,
x2,
x3,
x4) =
U1_GGA(
x1,
x2,
x4)
U4_GGA(
x1,
x2,
x3,
x4) =
U4_GGA(
x1,
x2,
x4)
U5_GGA(
x1,
x2,
x3,
x4) =
U5_GGA(
x1,
x2,
x4)
U6_GGA(
x1,
x2,
x3) =
U6_GGA(
x1,
x2,
x3)
GEQC_IN_GG(
x1,
x2) =
GEQC_IN_GG(
x1,
x2)
U2_GG(
x1,
x2,
x3) =
U2_GG(
x1,
x2,
x3)
We have to consider all (P,R,Pi)-chains
(5) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LOPSTR] contains 3 SCCs with 7 less nodes.
(6) Complex Obligation (AND)
(7) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
GEQC_IN_GG(s(X1), s(X2)) → GEQC_IN_GG(X1, X2)
The TRS R consists of the following rules:
subcB_in_gga(s(X1), X2, X3) → U13_gga(X1, X2, X3, subcD_in_gga(X1, X2, X3))
subcD_in_gga(s(X1), s(X2), X3) → U11_gga(X1, X2, X3, subcD_in_gga(X1, X2, X3))
subcD_in_gga(X1, 0, X1) → subcD_out_gga(X1, 0, X1)
U11_gga(X1, X2, X3, subcD_out_gga(X1, X2, X3)) → subcD_out_gga(s(X1), s(X2), X3)
U13_gga(X1, X2, X3, subcD_out_gga(X1, X2, X3)) → subcB_out_gga(s(X1), X2, X3)
The argument filtering Pi contains the following mapping:
s(
x1) =
s(
x1)
subcB_in_gga(
x1,
x2,
x3) =
subcB_in_gga(
x1,
x2)
U13_gga(
x1,
x2,
x3,
x4) =
U13_gga(
x1,
x2,
x4)
subcD_in_gga(
x1,
x2,
x3) =
subcD_in_gga(
x1,
x2)
U11_gga(
x1,
x2,
x3,
x4) =
U11_gga(
x1,
x2,
x4)
0 =
0
subcD_out_gga(
x1,
x2,
x3) =
subcD_out_gga(
x1,
x2,
x3)
subcB_out_gga(
x1,
x2,
x3) =
subcB_out_gga(
x1,
x2,
x3)
GEQC_IN_GG(
x1,
x2) =
GEQC_IN_GG(
x1,
x2)
We have to consider all (P,R,Pi)-chains
(8) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.
(9) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
GEQC_IN_GG(s(X1), s(X2)) → GEQC_IN_GG(X1, X2)
R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains
(10) PiDPToQDPProof (EQUIVALENT transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(11) Obligation:
Q DP problem:
The TRS P consists of the following rules:
GEQC_IN_GG(s(X1), s(X2)) → GEQC_IN_GG(X1, X2)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(12) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.
From the DPs we obtained the following set of size-change graphs:
- GEQC_IN_GG(s(X1), s(X2)) → GEQC_IN_GG(X1, X2)
The graph contains the following edges 1 > 1, 2 > 2
(13) YES
(14) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
SUBD_IN_GGA(s(X1), s(X2), X3) → SUBD_IN_GGA(X1, X2, X3)
The TRS R consists of the following rules:
subcB_in_gga(s(X1), X2, X3) → U13_gga(X1, X2, X3, subcD_in_gga(X1, X2, X3))
subcD_in_gga(s(X1), s(X2), X3) → U11_gga(X1, X2, X3, subcD_in_gga(X1, X2, X3))
subcD_in_gga(X1, 0, X1) → subcD_out_gga(X1, 0, X1)
U11_gga(X1, X2, X3, subcD_out_gga(X1, X2, X3)) → subcD_out_gga(s(X1), s(X2), X3)
U13_gga(X1, X2, X3, subcD_out_gga(X1, X2, X3)) → subcB_out_gga(s(X1), X2, X3)
The argument filtering Pi contains the following mapping:
s(
x1) =
s(
x1)
subcB_in_gga(
x1,
x2,
x3) =
subcB_in_gga(
x1,
x2)
U13_gga(
x1,
x2,
x3,
x4) =
U13_gga(
x1,
x2,
x4)
subcD_in_gga(
x1,
x2,
x3) =
subcD_in_gga(
x1,
x2)
U11_gga(
x1,
x2,
x3,
x4) =
U11_gga(
x1,
x2,
x4)
0 =
0
subcD_out_gga(
x1,
x2,
x3) =
subcD_out_gga(
x1,
x2,
x3)
subcB_out_gga(
x1,
x2,
x3) =
subcB_out_gga(
x1,
x2,
x3)
SUBD_IN_GGA(
x1,
x2,
x3) =
SUBD_IN_GGA(
x1,
x2)
We have to consider all (P,R,Pi)-chains
(15) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.
(16) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
SUBD_IN_GGA(s(X1), s(X2), X3) → SUBD_IN_GGA(X1, X2, X3)
R is empty.
The argument filtering Pi contains the following mapping:
s(
x1) =
s(
x1)
SUBD_IN_GGA(
x1,
x2,
x3) =
SUBD_IN_GGA(
x1,
x2)
We have to consider all (P,R,Pi)-chains
(17) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(18) Obligation:
Q DP problem:
The TRS P consists of the following rules:
SUBD_IN_GGA(s(X1), s(X2)) → SUBD_IN_GGA(X1, X2)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(19) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.
From the DPs we obtained the following set of size-change graphs:
- SUBD_IN_GGA(s(X1), s(X2)) → SUBD_IN_GGA(X1, X2)
The graph contains the following edges 1 > 1, 2 > 2
(20) YES
(21) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
REMA_IN_GGA(X1, s(X2), X3) → U4_GGA(X1, X2, X3, subcB_in_gga(X1, X2, X4))
U4_GGA(X1, X2, X3, subcB_out_gga(X1, X2, X4)) → REMA_IN_GGA(X4, s(X2), X3)
The TRS R consists of the following rules:
subcB_in_gga(s(X1), X2, X3) → U13_gga(X1, X2, X3, subcD_in_gga(X1, X2, X3))
subcD_in_gga(s(X1), s(X2), X3) → U11_gga(X1, X2, X3, subcD_in_gga(X1, X2, X3))
subcD_in_gga(X1, 0, X1) → subcD_out_gga(X1, 0, X1)
U11_gga(X1, X2, X3, subcD_out_gga(X1, X2, X3)) → subcD_out_gga(s(X1), s(X2), X3)
U13_gga(X1, X2, X3, subcD_out_gga(X1, X2, X3)) → subcB_out_gga(s(X1), X2, X3)
The argument filtering Pi contains the following mapping:
s(
x1) =
s(
x1)
subcB_in_gga(
x1,
x2,
x3) =
subcB_in_gga(
x1,
x2)
U13_gga(
x1,
x2,
x3,
x4) =
U13_gga(
x1,
x2,
x4)
subcD_in_gga(
x1,
x2,
x3) =
subcD_in_gga(
x1,
x2)
U11_gga(
x1,
x2,
x3,
x4) =
U11_gga(
x1,
x2,
x4)
0 =
0
subcD_out_gga(
x1,
x2,
x3) =
subcD_out_gga(
x1,
x2,
x3)
subcB_out_gga(
x1,
x2,
x3) =
subcB_out_gga(
x1,
x2,
x3)
REMA_IN_GGA(
x1,
x2,
x3) =
REMA_IN_GGA(
x1,
x2)
U4_GGA(
x1,
x2,
x3,
x4) =
U4_GGA(
x1,
x2,
x4)
We have to consider all (P,R,Pi)-chains
(22) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(23) Obligation:
Q DP problem:
The TRS P consists of the following rules:
REMA_IN_GGA(X1, s(X2)) → U4_GGA(X1, X2, subcB_in_gga(X1, X2))
U4_GGA(X1, X2, subcB_out_gga(X1, X2, X4)) → REMA_IN_GGA(X4, s(X2))
The TRS R consists of the following rules:
subcB_in_gga(s(X1), X2) → U13_gga(X1, X2, subcD_in_gga(X1, X2))
subcD_in_gga(s(X1), s(X2)) → U11_gga(X1, X2, subcD_in_gga(X1, X2))
subcD_in_gga(X1, 0) → subcD_out_gga(X1, 0, X1)
U11_gga(X1, X2, subcD_out_gga(X1, X2, X3)) → subcD_out_gga(s(X1), s(X2), X3)
U13_gga(X1, X2, subcD_out_gga(X1, X2, X3)) → subcB_out_gga(s(X1), X2, X3)
The set Q consists of the following terms:
subcB_in_gga(x0, x1)
subcD_in_gga(x0, x1)
U11_gga(x0, x1, x2)
U13_gga(x0, x1, x2)
We have to consider all (P,Q,R)-chains.
(24) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04,JAR06].
The following pairs can be oriented strictly and are deleted.
U4_GGA(X1, X2, subcB_out_gga(X1, X2, X4)) → REMA_IN_GGA(X4, s(X2))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:
POL(0) = 0
POL(REMA_IN_GGA(x1, x2)) = x1
POL(U11_gga(x1, x2, x3)) = 1 + x3
POL(U13_gga(x1, x2, x3)) = x3
POL(U4_GGA(x1, x2, x3)) = x3
POL(s(x1)) = 1 + x1
POL(subcB_in_gga(x1, x2)) = x1
POL(subcB_out_gga(x1, x2, x3)) = 1 + x3
POL(subcD_in_gga(x1, x2)) = 1 + x1
POL(subcD_out_gga(x1, x2, x3)) = 1 + x3
The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:
subcB_in_gga(s(X1), X2) → U13_gga(X1, X2, subcD_in_gga(X1, X2))
subcD_in_gga(s(X1), s(X2)) → U11_gga(X1, X2, subcD_in_gga(X1, X2))
subcD_in_gga(X1, 0) → subcD_out_gga(X1, 0, X1)
U13_gga(X1, X2, subcD_out_gga(X1, X2, X3)) → subcB_out_gga(s(X1), X2, X3)
U11_gga(X1, X2, subcD_out_gga(X1, X2, X3)) → subcD_out_gga(s(X1), s(X2), X3)
(25) Obligation:
Q DP problem:
The TRS P consists of the following rules:
REMA_IN_GGA(X1, s(X2)) → U4_GGA(X1, X2, subcB_in_gga(X1, X2))
The TRS R consists of the following rules:
subcB_in_gga(s(X1), X2) → U13_gga(X1, X2, subcD_in_gga(X1, X2))
subcD_in_gga(s(X1), s(X2)) → U11_gga(X1, X2, subcD_in_gga(X1, X2))
subcD_in_gga(X1, 0) → subcD_out_gga(X1, 0, X1)
U11_gga(X1, X2, subcD_out_gga(X1, X2, X3)) → subcD_out_gga(s(X1), s(X2), X3)
U13_gga(X1, X2, subcD_out_gga(X1, X2, X3)) → subcB_out_gga(s(X1), X2, X3)
The set Q consists of the following terms:
subcB_in_gga(x0, x1)
subcD_in_gga(x0, x1)
U11_gga(x0, x1, x2)
U13_gga(x0, x1, x2)
We have to consider all (P,Q,R)-chains.
(26) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.
(27) TRUE